Nuprl Lemma : binrel_eqv_functionality_wrt_breqv
13,42
postcript
pdf
T
:Type,
a
,
a'
,
b
,
b'
:(
T
T
).
(
a
<
>{
T
}
b
)
(
a'
<
>{
T
}
b'
)
((
a
<
>{
T
}
a'
)
(
b
<
>{
T
}
b'
))
latex
Up
gen
algebra
1
Definitions
x
,
y
.
t
(
x
;
y
)
,
t
T
,
,
x
:
A
.
B
(
x
)
,
P
Q
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Sym(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
P
&
Q
,
EquivRel(
T
;
x
,
y
.
E
(
x
;
y
))
,
{
T
}
,
x
(
s1
,
s2
)
Lemmas
binrel
eqv
wf
,
equiv
rel
self
functionality
,
binrel
eqv
weakening
,
binrel
eqv
inversion
,
binrel
eqv
transitivity
origin
T:Type, a, a', b, b':(T
T
).
>{T} b) 
(a' <>{T} b') ((a <>{T} a') 
(b <>{T} b')) T:Type, a, a', b, b':(TT).
>{T} b) (a' <>{T} b') ((a <>{T} a') (b <>{T} b')) 
x,y. t(x;y)
T